perm filename PARADO[E77,JMC] blob sn#293394 filedate 1977-07-12 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 00003	.skip to column 1
C00009 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.at "qf" ⊂"%Af%*"⊃
.at "qm1" ⊂"%5-1%*"⊃
.at "qg" ⊂"%Ag%*"⊃
.at "qx" ⊂"%8x%*"⊃
.at "q0" ⊂"%40%*"⊃
.turn on "↑"

.cb Notes on paradoxes and self-application

.item←0
#. Russell's paradox is the simplest.  Suppose that predicates are
can be applied to predicates unrestrictedly.  Then we define the
predicate ⊗h (for %2heterological%1) by

!!a1:	%2(∀x)(h(x) ≡ ¬x(x))%1.

Substituting ⊗h for ⊗x immediately gives

!!a2:	%2h(h) ≡ ¬h(h)%1

which is already a propositional calculus contradiction.


#. Let us now see how close we can come to translating Russell's paradox
into first order logic.  Let %2αα:AqxA_→_B%1 be a mapping and let
%2n:B_→_B%1 be a mapping such that

!!a9:	%2(∀b)(n_b_≠_b)%1,

i.e. ⊗n is a mapping without a fixed point.
We shall regard αα as an "apply" function that applies an element of ⊗A 
regarded as a mapping to another element of ⊗A regarded as an argument.
Therefore, we shall call %2qf:A_→_B%1 representable, if there is %2f_ε_A%1
such that

!!a6:	%2(∀a)(qf(a) = αα(f,a))%1.

For example, if ⊗A is taken as the set of S-expressions in LISP and
αα is taken as a LISP one-argument apply function, we are interested
in what functions from S-expressions to some other domain are representable.
Consider the function qfq0 defined by

!!a7:	%2qfq0(a) = n αα(a,a)%1.

We claim that qfq0 is not representable.  If it were represented by
some element %2aq0%1 of ⊗A, we would have

!!a8:	%2αα(aq0,aq0) = qfq0(aq0) = n αα(aq0,aq0)%1

which is not possible on account of ({eq a9}).

#. Cantor's proof that if a set ⊗B has more than
one element, then %2B↑A%1 cannot be put in 1-1 correspondence with
⊗A, can be reduced to the previous example.  Suppose that ⊗f takes
⊗A into %2B↑A%1.  We then define

!!a12:	%2αα(a1,a2) = f(a1)(a2)%1.

Since ⊗B is assumed to have at least two elements, a suitable function
⊗n exists and

!!a13:	%2qfq0(a) = n f(a)(a)%1,

and the fact that qfq0 is not representable tells us that the mapping
⊗f cannot be onto.

#. In λ-calculus, we can obtain a fixed point for any λ-expression ⊗f, namely

!!a10:	%2[λx.f(x(x))][λx.f(x(x))] = f[[λx.f(x(x))][λx.f(x(x))]]%1,

where the equality is established by a single λ-conversion of the
expression on the left.  The fixed point operator itself is therefore
given by

!!a11:	%2Y = λf.[λx.f(x(x))][λx.f(x(x))]%1.

#. The following LlSP expression non-trivially evaluates to itself:

((LAMBDA (X) (LIST X (LIST (QUOTE QUOTE) X))) (QUOTE (LAMBDA (X)
(LIST X (LIST (QUOTE QUOTE) X))))).

The fact that T and NIL also evaluate to themselves is an anomaly.
.skip to column 1
#. We shall now consider a translation of the paradox
into first order logic.  Let ⊗F be a set that we regard as representations
for certain functions from a set ⊗A to a set ⊗B.  We could, for example,
take both ⊗A and ⊗B as the set of S-expressions and take ⊗F as the
S-expression representation of a LISP function.
Thus there is a function αα:%2F_qx B_→_A%1 which could be taken as the
LISP ⊗apply function in the above example.  We will call a function
%2qf:B_→_A%1 representable iff there exists %2f_ε_F%1 such that

!!a3:	%2(∀b)(qf(b) = αα(f,b)%1.

Next let %2qg:F_→_B%1 be 1-1, i.e. qg represents elements of ⊗F by
elements of ⊗B.  In the example, qg can be taken as the identity
function.  Finally, let %2n:A_→_A%1 satisfy %2(∀a)(n(a)_≠_a)%1.
Now define

!!a4:	%2qf(b) = qif b ε qg(F) qthen n(αα(qgqm1 b,b)) qelse a%40%1,

where %2a%40%1 is an arbitrary element of ⊗A.  Suppose that qf were
representable by %2f_ε_F%1.  We would then have

!!a5:	%2αα(f,qg(f)) = qf(qg(f)) = n(αα(qgqm1(qg(f)),qg(f))) = n(αα(f,qg(f)))%1,

which is a contradiction, since ⊗n has been assumed to have no fixed point.